\begin{tabbing}
$\forall$$A$, $B$:Type, $g$:($A$$\rightarrow$($B$ + Top)), $X$:MaInterface($A$), ${\it es}$:ES, $i$:Id.
\\[0ex]($\uparrow$$i$ $\in$ dom($X$))
\\[0ex]$\Rightarrow$ \=(ma{-}interface{-}consistent{-}at(${\it es}$;$i$;$X$)\+
\\[0ex]$\Leftarrow\!\Rightarrow$ ma{-}interface{-}consistent{-}at(${\it es}$;$i$;ma{-}interface{-}compose($g$;$X$)))
\-
\end{tabbing}